x, y:Atom. ((x =a y))  x  y  Atom  

latex

ProofTree

Definitions	a  b  T , , t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x)
Lemmas	nequal wf, eq atom wf, assert wf, not wf